T:Type, L:(T List), x, y:T. adjacent(T;L;x;y)  x before y  L 

latex

ProofTree

Definitions

x:A  B(x), x:A. B(x), x:AB(x), x:A. B(x), i  j , ||as||, {i..j}, increasing(f;k), s = t, P & Q, Type, type List, , {x:A| B(x)} , t  T, #$n, n+m, l[i], , n - m, f(a), [], [car / cdr], (x  l), P  Q, L1  L2, x before y  l, adjacent(T;L;x;y), a < b, A  B, , i  j < k, <a, b>, -n, False, A, A c B, (i = j), if b then t else f fi , x.A(x), b, ff, b, tt, P  Q, x =a y, null(as), a < b, x f y, a < b, [d], p  q, p  q, p q, i <z j, i z j, Unit, left + right, hd(l), tl(l), {T}, SQType(T), s ~ t, P  Q, Dec(P), Atom, x,y:A//B(x;y), b | a, a ~ b, |p|, a  b, a <p b, |g|, a < b, |r|, xL. P(x), (xL.P(x))

Lemmas

decidable int equal, guard wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, not wf, assert wf, ifthenelse wf, le wf, increasing wf, int seg wf